$\forall$${\it the\_es}$:ES, $e$:E.
\\[0ex]($\uparrow$isrcv($e$))
\\[0ex]$\Rightarrow$ (snds(lnk($e$), before(sender($e$),index($e$))) = msgs(lnk($e$);before($e$)) $\in$ (Msg List))